\documentclass[a4paper]{article}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{hyperref}
\usepackage{graphicx}
\usepackage{geometry}

\geometry{
    letterpaper,
    left=   1.5in,
    right=  1.5in,
    top=    1.3in,
    bottom= 1.4in
}

\newcommand{\partd}[2]{\frac{\partial #1}{\partial #2}}
\newcommand{\dih}{\mathrel{\rm dih}}


\parindent=0mm
\parskip=5pt

\title{A Tool for Formal Verification of Nonlinear Inequalities}

\author{Alexey Solovyev}

% Document
\begin{document}
% Title
\maketitle

% Content
\tableofcontents

\pagebreak
% References
\begin{thebibliography}{9}
\bibitem{HOL} HOL Light home page\\
        \url{http://www.cl.cam.ac.uk/~jrh13/hol-light}

\bibitem{HOL-tutorial} HOL Light tutorial\\
        \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf}

\bibitem{flyspeck} The Flyspeck project\\
        \url{http://code.google.com/p/flyspeck/}

\bibitem{bernstein}C\'esar Mu\~noz and Anthony Narkawicz, {\it Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization}, Journal of Automated Reasoning, DOI: 10.1007/s10817-012-9256-3\\
        \url{http://shemesh.larc.nasa.gov/people/cam/Bernstein/}
\end{thebibliography}

% Introduction
\section{Introduction}
This document describes a tool for verification of nonlinear inequalities in HOL Light proof assistant~\cite{HOL, HOL-tutorial}. This tool was developed as a part of the Flyspeck project (a formal proof of the Kepler conjecture)~\cite{flyspeck}. The tool is capable to verify multivariate nonlinear strict inequalities on rectangular domains. More specifically, the tool can handle inequalities in the form
\[\forall {\bf x} \in D \implies f({\bf x}) < g({\bf x}),\]
where $D = \{(x_1, \ldots, x_n)\ |\ a_i \le x_i \le b_i\}$ and $f$, $g$ are functions which may include all usual arithmetic operations, square roots, arccosines, and arctangents. The maximal number of variables is 8. Future releases of the tool will include all elementary functions and will have no restriction on the number of variables. Moreover, it will be possible to verify inequalities on non-rectangular domains.

Internally, the tool uses interval arithmetic with Taylor approximations (with second-order error terms).

The document is organized as follows. The next section describes the installation process. Then a quick introduction of tool functions is presented. After that, a more detailed description of tool functions is given and special options are described. The last two sections describe several examples and test cases.


% Installation
\section{Installation}
First of all, if you don't have OCaml and HOL Light installed, then you need to install them. The verification tool was tested with Ocaml 3.09.3 and Ocaml 3.12.1 and with one of the latest versions of HOL Light (r149 in the HOL Light repository).  HOL Light installation instructions can be found in John Harrison's HOL Light tutorial~\cite{HOL-tutorial}.

Alternatively, one can download and run the following script written by Alex Krauss: \url{https://bitbucket.org/akrauss/hol-light-workbench}. This script will download and install the latest version of HOL Light and other necessary programs.

The installation of the tool for verification of nonlinear inequalities is very simple. Download the distribution from

\vspace{-5pt}
\url{http://code.google.com/p/flyspeck/downloads/list}

\vspace{-5pt}
or get the latest version from the Flyspeck repository with the shell command

\vspace{-5pt}
\verb|svn co http://flyspeck.googlecode.com/svn/trunk/formal_ineqs|


The tool can be placed in any directory on your computer. It is important to inform HOL Light about tool's location. It can be done with the following OCaml command:

\verb|load_path := "path to the tool directory" :: !load_path;;|

After the path is set, the tool can be loaded with the command

\verb|needs "verifier/m_verifier_main.hl";;|

The tool loads the standard HOL Light library \verb|Multivariate/realanalysis.ml|. The loading process of this library could take pretty long time, so it is recommended to use a checkpointed version of HOL Light with preloaded multivariate analysis libraries.

Before loading the tool, it is also possible to change some global options. These options are described in section \ref{global}.


% Examples
\section{Quick Start}

The polynomial inequality
\begin{multline*}
-\frac{1}{\sqrt{3}} \le x \le \sqrt{2},\ -\sqrt{\pi} \le y \le 1
\implies x^2 y - x y^4 + y^6 + x^4 - 7 > -7.17995
\end{multline*}
can be verified with the following script

\begin{verbatim}
(* make sure that load_path contains the path to formal_ineqs *)
needs "verifier/m_verifier_main.hl";;
open M_verifier_main;;

let ineq =
  `-- &1 / sqrt(&3) <= x /\ x <= sqrt(&2) /\
   -- sqrt(pi) <= y /\ y <= 1
   ==> x pow 2 * y - x * y pow 4 + y pow 6 - &7 + x pow 4 > -- #7.17995`;;

let th, stats = verify_ineq default_params 5 ineq;;
\end{verbatim}

The first parameter of the verification function \verb|verify_ineq| contains verification options. We use default values given by the constant \verb|default_params|. Available options are described in section \ref{verification}.

The second parameter specifies the precision of formal floating point operations. This parameter determines the maximal number of significant digits of any result returned by a formal floating point operation. Here, digits are not decimal. Internally all natural numbers are represented using a fixed base (see section \ref{global} for more details). This base is relatively large (the default value is 100) to speed up arithmetic operations. Actual precision of formal floating point operations depends on the precision parameter and on the base of the internal representation of natural numbers. If the base value is 100 and the precision parameter is 5 as in the example above, then the precision of formal floating point operations is 10 decimal digits: $100^5 = 10^{10}$. Note that the verification of the example will fail if the precision parameter is 4 or less. On the other hand, if the precision parameter is 10, the verification will succeed but it will take a little more time.

The third parameter is the inequality itself given as a HOL Light term. The format of this term is simple: it is an implication with bounds of variables in the antecedent and an inequality in the consequent. The bounds of all variables should be in the form $\text{\it a constant expression} <= x$ or $x <= \text{\it a constant expression}$. For each variable, upper and lower bounds must be given. The inequality must be a strict inequality ($<$ or $>$). The inequality may include \verb|sqrt|, \verb|atn|, and \verb|acs| functions. The constant \verb|pi| ($\pi$) is also allowed.

The verification function returns a HOL Light theorem and a record with some verification information which include verification time.


% Verification Functions
\section{Verification Functions}\label{verification}
The main verification function \verb|verify_ineq| is contained in \verb|M_verifier_main| module defined in \verb|verifier/m_verifier_main.hl|. The function has 3 arguments and its type is
\begin{verbatim}
verify_ineq : verification_parameters -> int -> term -> thm * verification_stats
\end{verbatim}

The first parameter contains verification options defined in the following record
\begin{verbatim}
type verification_parameters =
{
  (* If true, then monotonicity properties can be used *)
  (* to reduce the dimension of a problem *)
  allow_derivatives : bool;
  (* If true, then convexity can be used *)
  (* to reduce the dimension of a problem *)
  convex_flag : bool;
  (* If true, then verification on internal subdomains can be skipped *)
  (* for a monotone function *)
  mono_pass_flag : bool;
  (* If true, then raw interval arithmetic can be used *)
  (* (without Taylor approximations) *)
  raw_intervals_flag : bool;
  (* If true, then an informal procedure is used to determine *)
  (* the optimal precision for the formal verification *)
  adaptive_precision : bool;
  (* This parameter might be used in cases when the certificate search *)
  (* procedure returns a wrong result due to rounding errors *)
  (* (this parameter will be eliminated when the search procedure is corrected) *)
  eps : float;
};;
\end{verbatim}
A detailed description of these parameter is omitted in this document. In most cases, it is enough to use the constant \verb|default_params| which turns all verification flags on and sets \verb|eps = 0|. In rare cases, it is necessary to adjust \verb|eps| to get a result. This can be done with the command
\begin{verbatim}
verify_ineq {default_params with eps = 1e-10} 5 ineq_tm;;
\end{verbatim}

The second parameter of the verification function specifies the precision of formal floating point operations. This parameter determines the maximal number of significant digits of any result returned by a formal floating point operation. Here, digits are not decimal. Internally all natural numbers are represented using a fixed base (see section \ref{global} for more details). This base is relatively large (the default value is 100) to speed up arithmetic operations. Actual precision of formal floating point operations depends on the precision parameter and on the base of the internal representation of natural numbers. In many cases, if the verification function fails, it is enough to increase the precision parameter to get a result.

The third parameter of the verification function is a HOL Light term which specifies an inequality itself. The format of this term is the following:
\begin{verbatim}
bounds of variables ==> an inequality
\end{verbatim}
The bounds of all variables should be in the form $\text{\it a constant expression} <= x$ or $x <= \text{\it a constant expression}$. For each variable, upper and lower bounds must be provided. The order in which the bounds are given is irrelevant. Bounds of variables may be connected with \verb|/\| or with \verb|==>|. The inequality must be a strict inequality ($<$ or $>$). The inequality may include \verb|sqrt|, \verb|atn|, and \verb|acs| functions. The constant \verb|pi| ($\pi$) is also allowed.

The verification function returns a theorem and some verification information defined in the record
\begin{verbatim}
type verification_stats =
{
  total_time : float;
  formal_verification_time : float;
  certificate : Verifier.certificate_stats;
};;
\end{verbatim}
The field \verb|total_time| contains total verification time. The field \verb|formal_verification_time| contains time taken by the formal verification procedure only (this time doesn't include time for constructing a solution certificate and for other preparations). The last field \verb|certificate| contains information about a solution certificate.

The conclusion of the returned theorem is not exactly the same as the third parameter of the verification function: the order of bounds of variables may be altered and variables which are not used in the inequality are eliminated. For example, commands
\begin{verbatim}
let th1, _ = verify_ineq default_params 3
  `&1 <= y /\ y <= &2 /\ &1 <= x /\ x <= &3 ==> x + y < &6`;;
let th2, _ = verify_ineq default_params 3
  `&1 <= y /\ y <= &2 /\ &1 <= x /\ x <= &3 ==> y < &3`;;
\end{verbatim}
return
\begin{verbatim}
th1 = |- (&1 <= x /\ x <= &3) /\ &1 <= y /\ y <= &2 ==> x + y < &6
th2 = |- &1 <= y /\ y <= &2 ==> y < &3
\end{verbatim}



% Options
\section{Global Options}\label{global}
The options which affect the arithmetic operations with natural and floating point numbers must be set before the verification tool is loaded. After the verification tool is loaded, arithmetic options may not be changed. To set arithmetic options, load the file \verb|arith_options.hl| located in the root directory of the tool. The available options are listed below.

\begin{enumerate}
% base
\item[\bf base] Determines the base for representing natural numbers. Default HOL Light
representation of natural numbers is binary (i.e., its base is 2). A higher base increases speed of arithmetic operations but it also requires more memory to remember additional theorems. The default value of the base is \verb|100|. To set a new base, use the command

\verb|Arith_options.base := 200;;|

% min_exp
\item[\bf min\_exp] Determines the minimal exponent in the representation of floating point numbers. Each floating point number is represented as a triple $(s, n, e)$ where $s$ is a boolean value which determines the sign of the number, $n$ and $e$ are natural numbers which represent the mantissa and the exponent. The value corresponding to $(s, n, e)$ is given by

\[f = (-1)^{\text{if $s$ then $1$ else $0$}} \times n \times b^{e - min\_exp}\]
where $b$ is the base of the representation of natural numbers.

% cached
\item[\bf cached] If this value is true, then results of all natural number operations are cached. The default value is \verb|true|.

% float_cached
\item[\bf float\_cached] If this value is true, then results of all floating point operations are cached. The default value is \verb|true|.

% init_cache_size
\item[\bf init\_cache\_size] Determines the initial size of the cache for results of arithmetic operations. The default value is \verb|10000|.

% max_cache_size
\item[\bf max\_cache\_size] Determines the maximal size of the cache for results of arithmetic operations. The default value is \verb|20000|. Note: each cached operation has its own cache.

\end{enumerate}

The file \verb|verifier_options.hl| contains the option \verb|info_print_level| which controls the amount of information printed by a verification process. This option can be changed at any time:

\verb|Verifier_options.info_print_level := 0;;|

Possible values are: 0~(no information is printed); 1~(all essential information is printed); 2~(all information is printed). The default value is 1.

The next example shows how to change default options:
\begin{verbatim}
(* The arithmetic options must be set before loading the verification tool *)
needs "arith_options.hl";;

(* Increase the arithmetic base *)
Arith_options.base := 200;;

(* Increase the cache size *)
Arith_options.max_cache_size = 40000;;

(* Load the verification tool *)
needs "verifier/m_verifier_main.hl";;

(* The verification option can be changed at any time *)
Verifier_options.info_print_level := 2;;

open M_verifier_main;;
\end{verbatim}

% Additional Examples
\section{Additional Examples}
The verification tool distribution contains several example files. The file \verb|examples_poly.hl| contains polynomial inequalities from the paper \cite{bernstein}. The command

\verb|needs "examples_poly.hl";;|

will load this file and run all polynomial inequality tests. To run all tests again, type \verb|run_tests();;|

To run a specific test, type \verb|run_{test_name}();;| where \verb|{test_name}| is one of the following: \verb|schwefel|, \verb|rd|, \verb|caprasse|, \verb|lv|, \verb|butcher|, \verb|magnetism|, \verb|heart|.

Here is the list of all examples.
\begin{itemize}
% schwefel
\item[\bf schwefel]
\begin{eqnarray*}
&-5.8806 \times 10^{-10} < (x_1 - x_2^2)^2 + (x_2 - 1)^2 + (x_1 - x_3^2)^2 + (x_3 - 1)^2\\
&(x_1, x_2, x_3) \in [(-10,-10,-10),(10,10,10)]
\end{eqnarray*}

% rd
\item[\bf rd]
\begin{eqnarray*}
&-36.7126907 < -x_1 + 2 x_2 - x_3 - 0.835634534\, x_2 (1 + x_2)\\
&(x_1, x_2, x_3) \in [(-5,-5,-5),(5,5,5)]
\end{eqnarray*}

% caprasse
\item[\bf caprasse]
\begin{eqnarray*}
&-3.1801 < -x_1 x_3^3 + 4 x_2 x_3^2 x_4 + 4 x_1 x_3 x_4^2 + 2 x_2 x_4^3 + 4 x_1 x_3 + 4 x_3^2 - 10 x_2 x_4 - 10 x_4^2 + 2\\
&(x_1, x_2, x_3, x_4) \in [(-0.5,-0.5,-0.5,-0.5),(0.5,0.5,0.5,0.5)]
\end{eqnarray*}

% lv
\item[\bf lv]
\begin{eqnarray*}
&-20.801 < x_1 x_2^2 + x_1 x_3^2 + x_1 x_4^2 - 1.1 x_1 + 1\\
&(x_1, x_2, x_3, x_4) \in [(-2,-2,-2,-2), (2,2,2,2)]
\end{eqnarray*}

% butcher
\item[\bf butcher]
\begin{eqnarray*}
&-1.44 < x_6 x_2^2 + x_5 x_3^2 - x_1 x_4^2 + x_4^2 - \frac{1}{3} x_1 + \frac{4}{3} x_4\\
&(x_1, x_2, x_3, x_4, x_5, x_6) \in [(-1,-0.1, -0.1, -1, -0.1, -0.1), (0,0.9,0.5,-0.1,-0.05,-0.03)]
\end{eqnarray*}

% magnetsim
\item[\bf magnetism]
\begin{eqnarray*}
&-0.25001 < x_1^2 + 2 x_2^2 + 2 x_3^2 + 2 x_4^2 + 2 x_5^2 + 2 x_6^2 + 2 x_7^2 - x_1\\
&(x_1,x_2,x_3,x_4,x_5,x_6,x_7) \in [(-1,-1,-1,-1,-1,-1,-1), (1,1,1,1,1,1,1)]
\end{eqnarray*}

% heart
\item[\bf heart]
\begin{equation*}
\begin{split}
&-1.7435 < -x_1 x_6^3 + 3 x_1 x_6 x_7^2 - x_3 x_7^3 + 3 x_3 x_7 x_6^2 - x_2 x_5^3 + 3 x_2 x_5 x_8^2 - x_4 x_8^3 + 3 x_4 x_8 x_5^2 - 0.9563453\\
&(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8) \in [(-0.1, 0.4, -0.7, -0.7, 0.1, -0.1, -0.3, -1.1),\\ &\phantom{(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8) \in [ }(0.4, 1, -0.4, 0.4, 0.2, 0.2, 1.1, -0.3)]
\end{split}
\end{equation*}
\end{itemize}

The file \verb|examples_flyspeck.hl| contains some inequalities from the Flyspeck project~\cite{flyspeck}. The command

\verb|needs "examples_flyspeck.hl";;|

will load this file and run some easy inequality tests. To rerun these tests, use the command \verb|test_easy();;|. To run more difficult tests, type \verb|test_medium();;| or \verb|test_hard();;|.
(Warning: medium tests require about 30 minutes, hard tests require more than 5 hours.)

Some Flyspeck inequalities are listed below.
\begin{eqnarray*}
\Delta(x_1,\ldots,x_6) &= &x_1 x_4(-x_1 + x_2 + x_3 - x_4 + x_5 + x_6)\\
&& + x_2 x_5(x_1 - x_2 + x_3 + x_4 - x_5 + x_6)\\
&& + x_3 x_6(x_1 + x_2 - x_3 + x_4 + x_5 - x_6)\\
&& - x_2 x_3 x_4 - x_1 x_3 x_5 - x_1 x_2 x_6 - x_4 x_5 x_6,\\[6pt]
\Delta_4 &=& \partd{\Delta}{x_4},\\[6pt]
\dih_x(x_1,\ldots,x_6) &=& \frac{\pi}{2} - \arctan\left(\frac{-\Delta_4(x_1,\ldots,x_6)}{\sqrt{4 x_1 \Delta(x_1,\ldots,x_6)}}\right),\\[6pt]
\dih_y(y_1,\ldots,y_6) &=& \dih_x(y_1^2, \ldots, y_6^2).
\end{eqnarray*}

\begin{itemize}
% 1
\item[\bf 4717061266]
\begin{eqnarray*}
\Delta(x_1, x_2, x_3, x_4, x_5, x_6) > 0,\quad 4 \le x_i \le 6.3504
\end{eqnarray*}

% 2
\item[\bf 7067938795]
\begin{eqnarray*}
&\dih_x (x_1, \ldots, x_6) - \pi/2 + 0.46 < 0,\\
&4 \le x_{1,2,3} \le 6.3504,\ x_4 = 4,\ 3.01^2 \le x_{5,6} \le 3.24^2
\end{eqnarray*}

% 3
\item[\bf 3318775219]
\begin{eqnarray*}
&\begin{split}
0 < &\dih_y (y_1, \ldots, y_6) - 1.629 + 0.414 (y_2 + y_3 + y_5 + y_6 - 8.0)\\
        &- 0.763 (y_4 - 2.52) - 0.315 (y_1 - 2.0),
\end{split}\\
&2 \le y_i \le 2.52
\end{eqnarray*}

\end{itemize}

% Test Results
\section{Test Results}
This section contains time test results for inequalities described in the previous section. All tests were performed on Intel Core i5, 2.67GHz running Ubuntu 9.10 inside Virtual Box 4.2.0 on a Windows 7 host; the Ocaml version was 3.09.3; the base of arithmetic was 200; the caching was turned on.

\begin{center}
Polynomial inequalities

\begin{tabular}{l@{\quad} r r r r r}
%{r@{\quad}rl}
\hline
\multicolumn{1}{l}{\rule{0pt}{12pt}Inequality ID}&
\multicolumn{1}{l}{\phantom{x}\# variables}&
\multicolumn{1}{l}{\phantom{x}precision}&
\multicolumn{1}{l}{\phantom{x}total time (s)}&
\multicolumn{1}{l}{\phantom{x}formal verification (s)}\\
\hline\rule{0pt}{12pt}%
schwefel        & 3     & 5             & 26.329 &      19.145 \\
rd                      & 3 & 5         & 1.593 &       0.017 \\
caprasse        & 4 & 5         & 8.057 &       1.286 \\
lv                      & 4     & 5             & 1.875 &       0.030 \\
butcher         & 6 & 5         & 3.609 &       0.035 \\
magnetism       & 7 & 5         & 7.007 &       1.347 \\
heart           & 8 & 5         & 17.298 &      1.277 \\
\hline
\end{tabular}
\end{center}

\begin{center}
Flyspeck inequalities

\begin{tabular}{l@{\quad} r r r r r}
%{r@{\quad}rl}
\hline
\multicolumn{1}{l}{\rule{0pt}{12pt}Inequality ID}&
\multicolumn{1}{l}{\phantom{x}precision}&
\multicolumn{1}{l}{\phantom{x}total time (s)}&
\multicolumn{1}{l}{\phantom{x}formal verification (s)}\\
\hline\rule{0pt}{12pt}%
2485876245a     & 4 & 5.530 & 0.058 \\
4559601669b & 4 & 4.679 & 0.048 \\
4717061266  & 4 & 27.1 & 0.250 \\
5512912661  & 4 & 8.860 & 0.086 \\
6096597438a & 4 & 0.071 & 0.071 \\
6843920790  & 4 & 2.824 & 0.076 \\
SDCCMGA b   & 4 & 9.012 & 0.949 \\
TSKAJXY-TADIAMB\footnotemark[1] & 4 & 75.9 & 21.2 \\
7067938795  & 4 & 431   & 387 \\
5490182221  & 4 & 1726  & 1533 \\
3318775219  & 4 & 17091 & 15226 \\
\hline
\end{tabular}
\end{center}
\footnotetext[1]{Reduced to a polynomial inequality}

\end{document}



